Code (Week 8)

1. Sized Vectors
2. Subvectors (optional)

1 Sized Vectors

Some more examples on sized vectors, inculding some requiring explitic casts to type check. I won't expect anyone to be able to write such a program with explicit casts in the exam, but you should understand which types can be checked automatically, and the limits of sized vectors.

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE  RankNTypes, PolyKinds, TypeInType #-}
module Vector where

import Data.Proxy
import Data.Type.Equality

import Prelude hiding ((++))

data Nat = Z | S Nat

type family (+) (n :: Nat) (m :: Nat) :: Nat
type instance 'Z     + m = m
type instance ('S n) + m = 'S (n + m)

data SNat (n :: Nat) where
  Zero :: SNat Z
  Succ :: SNat m -> SNat (S m)


data Vec a (n :: Nat)  where
  Nil   :: Vec a 'Z 
  (:::) :: a -> Vec a n -> Vec  a ('S n) 

deriving instance Show a => Show (Vec a n)

vHead :: Vec a ('S n) -> a
vHead (x ::: xs) = x

vTail :: Vec a ('S n)  -> Vec a n 
vTail (x ::: xs) = xs

vMap :: (a -> b) -> Vec a n -> Vec b n
vMap f Nil = Nil
vMap f (x ::: xs) = (f x) ::: (vMap f xs)

-- can't return a sized vector, as number of output elements
-- unknown.
removeOdd :: Vec Int n -> [Int]
removeOdd Nil 
  = []
removeOdd (x ::: xs)
  | odd x     = removeOdd xs
cd  | otherwise = x : (removeOdd xs)

(++) :: Vec a n -> Vec a m -> Vec a (n + m) 
Nil        ++ xs = xs
(x ::: xs) ++ ys = x ::: (xs ++ ys) 

{- optional exercise: replace the XXX with theorems given below
   to get reverse to type check (the type error message which you 
   get when removing gcastWith XXX will tell you what's missing)

vReverse :: Vec a n -> Vec a n
vReverse vs =  gcastWith XXX $ rev' vs Nil 
  where
    rev' :: Vec a n -> Vec a m -> Vec a (n + m)
    rev' Nil ws 
      = ws
    rev' (v ::: vs) ws 
      = gcastWith XXX $ rev' vs (v ::: ws)
-}

merge :: Vec Int n  -> Vec Int m -> Vec Int (n + m)
merge Nil ys 
  = ys 
merge xs Nil 
  = gcastWith (plus_id_rv xs) xs
merge v1@(x ::: xs) v2@(y ::: ys) 
  | x <= y     = x ::: (merge xs v2)
  | otherwise  = gcastWith (plus_succ_idv v1 ys)  (y ::: (merge v1 ys))

plus_id_rv :: Vec a n -> ((n + Z) :~: n)
plus_id_rv Nil        = Refl       
plus_id_rv (x ::: xs) = gcastWith (plus_id_rv xs) Refl 


-- type level proof that  (Vec a (n + (S m)) ~ Vec a (S (n + m))
plus_succ_idv :: Vec a n1 -> Vec a n2 -> ((n1 + (S n2)) :~: (S (n1 + n2)))
plus_succ_idv Nil ws 
  = Refl
plus_succ_idv (v ::: vs) ws 
  = gcastWith (plus_succ_idv vs ws) Refl

-- type level proof that  n + (S m)) ~ S (n+ m)
plus_succ_id :: SNat n1 -> SNat n2 -> ((n1 + (S n2)) :~: (S (n1 + n2)))
plus_succ_id Zero n 
  = Refl
plus_succ_id (Succ x) n 
  = gcastWith (plus_succ_id x n) Refl


plus_id_r :: SNat n -> ((n + Z) :~: n)
plus_id_r Zero        
  = Refl       
plus_id_r (Succ n) 
  = gcastWith (plus_id_r n) Refl 




{- Example of a more complex proof:

   Could be done more compactly, but this way, every step is explicit and
   corresponds to the proof you would do on paper

   transitivity combines two equalities:     
   trans:: a :~: b) -> (b :~: c) -> (a :~: c)

  Induction step: I.H.: n1 + n2 = n2 + n1

 Sn1 + n2
 = {def of + }
 S(n1 + n2)
 = I.H.
 S(n2 + n1)
 = {plus_succ_id}
 (n2 + Sn1)
 -}

-- proof that + is commutative
plus_comm :: SNat n1 -> SNat n2 -> ((n1 + n2) :~: (n2 + n1))
plus_comm Zero m      
  = gcastWith (plus_id_r m) Refl
plus_comm (Succ n) m  
  = step4 n m plus_comm 


step4 ::  SNat n1 -> SNat n2 -> 
     (SNat n1 -> SNat n2 -> ((n1 + n2) :~: (n2 + n1))) -> 
          ((S n1 + n2) :~: (n2 +  S n1))
step4 n m ih = trans (step2 n m ih) (step3 n m)


step3 ::  SNat n1 -> SNat n2 -> (S(n2 + n1) :~: (n2 + S (n1)))
step3 n m =  (sym (plus_succ_id m n))

step2 ::  SNat n1 -> SNat n2 -> 
          (SNat n1 -> SNat n2 -> ((n1 + n2) :~: (n2 + n1))) -> 
          (((S n1) + n2) :~: (S(n2 + n1)))
step2 n m indHyp = trans Refl (step1 n m indHyp)

step1 ::  SNat n1 -> SNat n2 -> 
         (SNat n1 -> SNat n2 -> 
         ((n1 + n2) :~: (n2 + n1))) -> 
         (S(n1 + n2) :~: (S(n2 + n1)))
step1 n m indHyp = apply Refl (indHyp n m)

-- lifts a type equality on SNats to Vecs
vec_lift:: (SNat n -> (k :~: l)) -> 
           Vec a n -> (Vec a k :~: Vec a l)
vec_lift fn v  = apply Refl (fn (len v))
  where
    len ::Vec a n -> SNat n
    len Nil       = Zero
    len (x ::: xs) = Succ (len xs)


vec_lift2:: (SNat n -> SNat m -> (k :~: l)) -> 
           Vec a n -> Vec a m -> (Vec a k :~: Vec a l)
vec_lift2 fn v w = apply Refl (fn (len v) (len w))
  where
    len ::Vec a n -> SNat n
    len Nil       = Zero
    len (x ::: xs) = Succ (len xs)

2 Subvectors (optional)

The removeOdd function in the previous example code returns a list, as the size of the result can't be determined just by looking at the size of the input vector. See below for an alternative implementation, which encodes the fact the result is at most as big as the argument in the type. In practice, this is a pretty weak assertion, and in most cases, it wouldn't be worthwhile to go the extra length to encode it in the type.

{-# LANGUAGE GADTs, DataKinds, TypeFamilies  #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{-# FlexibleContexts #-}

module EvenV where

data Nat = Z | S Nat

data Vec a (n :: Nat)  where
    Nil   ::                 Vec a Z 
    (:::) :: a -> Vec a n -> Vec a (S n) 

class LTE (m :: Nat) (n :: Nat) where

instance LTE Z Z where

instance LTE Z (S n) where

instance LTE m n => LTE (S m) (S n) where

instance {-# OVERLAPS #-} LTE m n => LTE m (S n)


data SubVec a (n :: Nat)  where
     SV :: LTE m n => Vec a m -> SubVec a n

svcons :: a -> SubVec a n -> SubVec a (S n) 
svcons x (SV xs) = SV (x ::: xs)

svup :: SubVec a n  -> SubVec a (S n) 
svup (SV xs) = SV xs

removeOdd :: Vec Int n -> SubVec Int n
removeOdd Nil = SV Nil
removeOdd  (x ::: xs) 
 | even x    = svcons x (removeOdd xs)
 | otherwise = svup (takeEven xs)

Code (Week 8)

Table of Contents

1 Sized Vectors

2 Subvectors (optional)